(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Import Reals.
Open Scope R_scope.
Require Export Matrix.Mat.RMatrix.
Require Export Matrix.Mat.RMtacs.

(** Sg -> Sk *)

(* 水平面转动角度 φ   *)
Parameter phi  : R.

(* 对称面转动角度 μ ) *)
Parameter my  : R.

(* Sg在水平面转动φ度到过度坐标系S' *)
Definition coordinate_SgS' : Mat R 3 3 := mkMat_3_3
  (cos phi)  (sin phi) 0
  (-sin phi) (cos phi) 0
      0          0     1.


(* 再在飞机对称面转动μ度得到Sk *)
Definition coordinate_S'Sk : Mat R 3 3 := mkMat_3_3
  (cos my)   0 (-sin my)
     0       1    0
  (sin my)   0 (cos my).

(* 最后可得到Sg到Sk的转换 *)
Definition coordinate_SgSk : Mat R 3 3 := mkMat_3_3
  ((cos my)*(cos phi))  ((cos my)*(sin phi)) (-sin my)
  (-sin phi)                  (cos phi)          0
  ((sin my)*(cos phi))  ((sin my)*(sin phi))  (cos my).

(* multiplication of S'Sk and SgS' *)
Definition mul_S'Sk_SgS' := 
  RMmul coordinate_S'Sk coordinate_SgS'.

(* verify S'Sk * SgS' = SgSk *)
Lemma S'Sk_mul_SgS'_eq_SgSk : 
    coordinate_SgSk === mul_S'Sk_SgS'.
Proof.
  unfold mul_S'Sk_SgS'.
  unfold coordinate_SgSk.
  RMat_mul_simpl. unfold mkMat_3_3'.
  f_equal3.
Qed.
